
In this paper
we have studied %the expressiveness and decidability of a 
the expressiveness and decidability of 
higher-order process calculi featuring \emph{limited forwarding}. 
Our study has been centered around
\hof, 
the fragment of \hocore
%a higher-order process calculus 
%featuring a limited form of hig\-her-order communication.
%In \hof, 
%We have introduced \hof, a minimal higher-order calculus 
in which 
output actions can only include  
previously rece\-ived processes in composition with closed ones.
This communication style is reminiscent of programming 
%abstractions/paradigms 
scenarios
with forms of  
code mobility in which the recipient is not authorized or capable of accessing/modi\-fying the structure of the received code.
%The limitation in output actions represents a 
We have shown that such a 
weakening of the forward capabilities 
of higher-order processes %. Here we have shown it also  
has  consequences both on the expressiveness of the language and on the
decidability of termination. %We discuss on both issues next. 
Furthermore, we analyzed the extension of \hof with a \emph{passivation} operator
as a way of recovering the expressive power lost when moving from \hocore to \hof.

%As for the expressiveness issues, b
By exhibiting an  encoding of Minsky machines into \hof, we have shown that convergence is undecidable. 
% Hence, from an \emph{absolute expressiveness} standpoint, \hof is Turing complete. 
% Now, given the analogous result for \hocore \cite{LanesePSS08}, a
% \emph{relative expressiveness} issue also arises. 
% %Since % the encoding into \hocore, the 
% Indeed, 
% our encoding of Minsky machines into \hof is not faithful, which  
% reveals a difference on the criteria each encoding satisfies.
% \longv{
% This reminds us of the situation in \cite{Bravetti09}, for encodings of Turing complete formalisms into calculi with interruption and compensation. That work offers a detailed comparison of the criteria faithful and unfaithful encodings satisfy.
% For 
% the sake of conciseness, 
% %space, 
% we do not elaborate further on their  exact definition; 
% using the terminology in \cite{Bravetti09}, here it suffices to say that the presented encoding satisfies a  
% \emph{weakly Turing completeness} criterion, as opposed to the (stronger) \emph{Turing completeness} criterion that is satisfied by the encoding of Minsky machines into \hocore in \cite{LanesePSS08}. }
% \shortv{This reminds us of the situation in \cite{Bravetti09}, where faithful and unfaithful  encodings of Turing complete formalisms into calculi with interruption and compensation are compared.
% Using the terminology in \cite{Bravetti09}, we can say that the presented encoding satisfies a  
% \emph{weakly Turing completeness} criterion, as opposed to the (stronger) \emph{Turing completeness} criterion that is satisfied by the encoding of Minsky machines into \hocore in \cite{LanesePSS08}. }
Unlike the encoding of Minsky machines in \hocore, 
the encoding in \hof is not faithful. 
Hence, in the terminology of \cite{Bravetti09}, 
while \hocore is Turing complete, \hof is only \emph{weakly} Turing complete. 
This  discrepancy on the criteria satisfied by each encoding 
%might be interpreted as 
reveals
an expressiveness gap between \hof and \hocore; nevertheless, 
it seems clear that the loss of expressiveness resulting from limiting the forwarding capabilities in \hocore 
is much less dramatic than what one would have expected. 
%it seems clear that such a difference represents a much less dramatic loss of expressiveness
%than the one could have expected.
%

We have shown that the communication style of \hof causes a separation result with respect to \hocore.
In fact, because of the limitation on output actions, it was possible to prove that termination  in \hof is decidable.
This is in sharp contrast with the situation in \hocore, for which termination is undecidable.
In \hof, it is possible to provide an upper bound on the depth (i.e., the level of nesting of actions) of the
(set of) derivatives of a process. In \hocore such an upper bound does not exist.
This was shown to be essential for obtaining the decidability result; 
%to be able to prove the decidability of termination; for doing so 
for this, we appealed to the approach developed in \cite{Busi09}, which relies on 
% fixed bound for the derivatives of a given process, which is given in terms of the depth of (the syntax tree of) a process. By appealing by a proof strategy 
the theory of well-structured transition systems \cite{Finkel90,AbdullaCJT00,FinkelS01}.
As far as we are aware, this approach to studying expressiveness issues has not previously been used in the higher-order setting.
The decidability of termination 
is significant, as it might shed light 
on the development of verification techniques for higher-order processes.

We have also studied the expressiveness and decidability of \hopf,
the extension of \hof with a passivation operator.
To the best of our knowledge, this is the first expressiveness study involving 
passivation operators in the context of higher-order process calculi.
In \hopf it is possible to encode Minsky machines in a \emph{faithful} manner.
Hence, similarly as in \hocore, in \hopf both termination and convergence are undecidable.
This certainly does not imply that 
both languages have the same expressive power; 
in fact, 
an interesting direction for future work consists in 
assessing the exact expressive power that passivation brings into the picture.
This would include not only a comparison between \hopf and \hocore, but also
a comparison between \hocore and \hocore extended with passivation.
All the languages involved are Turing complete, hence 
such comparisons should employ techniques different from the ones used here.
%Related to this, i
It is also worth remarking that we have considered a very simple form of passivation,
one in which process suspension takes place with a considerable degree of non-determinism.
Studying other forms of passivation, possibly with more explicit control mechanisms, 
could be interesting from several points of view, including expressiveness.

%It is worth recalling that 
The \hof calculus is a sublanguage of \hocore.
%, a core higher-order process calculus studied in \cite{LanesePSS08}. 
As such, \hof inherits the many results and properties of \hocore; % \cite{LanesePSS08}; 
most notably, a notion of (strong) bisimilarity which is decidable and coincides with a number of sensible equivalences in the higher-order context.
Our results thus complement those in 
\cite{LanesePSS08} 
%previous chapters
and 
%provide a more complete picture 
deepen our understanding 
of the expressiveness of core higher-order calculi as a whole. 
Furthermore, by recalling that CCS without restriction is not Turing complete and has decidable convergence, 
the present results shape an interesting  expressiveness hierarchy, namely one in which 
\hocore is strictly more expressive than \hof (because of the discussion above), and in which 
\hof is strictly more expressive than CCS without restriction.



Remarkably, %we can easily extend 
our undecidability result %proving 
can be used to prove
that (weak) barbed bisimilarity is
undecidable in the 
%a higher-order 
calculus obtained by extending \hof with restriction.
Consider the encoding of Minsky
machines used in Section~\ref{s:turing} 
to prove the undecidability of 
convergence in \hof.
Consider now the restriction operator
$(\nu \tilde{x})$ used as a binder for
the names in the tuple $\tilde x$.
Take a Minsky machine $N$ (it is not
restrictive to assume that it executes
at least one increment instruction)
and its encoding $P$, as given by Definition~\ref{d:mmconfig}.
Let $\tilde{x}$ be the tuple of the names used by $P$, excluding the name $w$.
We have that $N$ terminates if and only
if $(\nu \tilde{x})P$ is (weakly) barbed equivalent to
the process $(\nu d)(\overline{d}|d|d.(\overline{w}|!w.\overline{w}))$.

%\shortv{\noindent {\bf Related Work.}}
%\longv{
\paragraph{\bf Related Work.}
% I commented this line (as well as all other citations of the LICS paper) for thesis purposes
%The most closely related work is \cite{LanesePSS08}, which was already discussed along the paper.
We do not know of other works that study the expressiveness of higher-order calculi by 
restricting higher-order outputs. 
%To the best of our knowledge, this is the first time decidable fragments of higher-order calculi are obtained by appealing to sublanguages that limit the power of higher-order output. 
The recent work \cite{BundgaardGHH09} studies 
%decidable fragments of 
%Homer, a higher-order process calculus with locations. 
%That work aims at 
 finite-control fragments of Homer \cite{Mikkel04}, a higher-order process calculus with locations.
While we have focused on decidability of termination and convergence, 
 in \cite{BundgaardGHH09} the interest is in decidability of barbed bisimilarity.
One of the approaches explored in \cite{BundgaardGHH09} is based on a type system that bounds the size of processes in terms 
of their syntactic components (e.g. number of parallel components, location nesting). 
%The second approach exploits results for the $\pi$-calculus and uses an encoding of $\pi$ into Homer to transport them in the form of a suitable subcalculus. 
Although the restrictions such a type system imposes might be considered 
as similar in spirit to the limitation on outputs in \hof (in particular, location nesting resembles the output nesting \hof forbids), the fact that the synchronization discipline in Homer 
depends heavily on the structure of locations makes it difficult to establish a more detailed comparison with \hof.  % between the works. 

Also similar in spirit to our work, but in a slightly different context, 
are some studies on the
expressiveness (of fragments) 
of the Ambient calculus \cite{CardelliG00}. 
Ambient and higher-order calculi are related 
in that both allow the communication of objects with complex structure.
Some works on the expressiveness of fragments of Ambient calculi are similar to ours.
In particular, 
\cite{BusiZ04} shows that termination is decidable for the fragment
without both restriction (as \hof and \hocore) and movement capabilities, and 
featuring replication; in contrast, the same property turns out to be undecidable 
for the fragment with recursion. 
%As \hof and \hocore, the Ambient fragments considered in \cite{BusiZ04} does not consider restriction.
Hence, the separation between fragments comes from the source of infinite behavior, and not from the structures allowed in output action, as in our case. 
%Then, in \cite{MaffeisP05}, it is shown that the construct for dissolving ambients can be ruled while preserving Turing completeness. 
However, we find that the connections
% that the conceptual differences 
between Ambient-like and higher-order calculi are rather loose, 
%significant, and 
so a proper comparison is difficult also in this case. 

% THIS IS TO BE UNCOMMENTED IN A JOURNAL VERSION....
% \paragraph{\bf Future Work.}
% As already mentioned, a great deal of the expressive power in higher-order calculi resides in the interplay of input and output actions.
% Here we have studied an alternative for limiting output capabilities; it would be interesting to investigate if suitable limitations on input actions are possible, and whether they have influence on expressiveness.
% %Such limitations could be related to, for instance, the linearity in execution  and/or forwarding. 
% Another interesting direction would be to compare higher-order and Ambient calculi from the expressiveness point of view.
% %, which, as mentioned before, share a number conceptual principles.
% 
 \paragraph{\bf Acknowledgments.}
 We are grateful to Julian Gutierrez and Roland Meyer 
 for their useful remarks on a previous version of this paper. 
